package Datalog
import DatalogAtom.createAtom

object DLToSROIQTransformer {
  private var variablecounter = 0

  def normalize(rule: DatalogRule): DatalogRule = {
    /* normalizes B and H */
    def normalize_h(rule: DatalogRule, oldRule: DatalogRule): DatalogRule = {
      val partiallyNormalized = normalizePartially(rule)
      val newAtoms = for (atom <- partiallyNormalized.atomList) yield replaceConstant(atom)
      val newResolution = replaceConstant(rule.givenResolution)
      val newAtomsAdd = for (atom <- newAtoms.map(tuple => tuple._2) if atom != null) yield atom
      
      // Calculate the body of the upcoming rule
      val body = if (newResolution._2 == null) newAtoms.map(tuple => tuple._1) ::: newAtomsAdd
      		else newResolution._2 :: newAtoms.map(tuple => tuple._1) ::: newAtomsAdd
      val newRule = new DatalogRule(body, newResolution._1)

      if (newRule == oldRule)
        newRule
      else
        normalize_h(newRule, newRule)
    }
    normalize_h(rule, rule)
  }

  /* Return value: (replaceAtom, appendAtom) */
  def replaceConstant(atom: DatalogAtom): (DatalogAtom, DatalogAtom) = atom.terms match {
    case Nil => throw new Exception()
    case x :: Nil =>
      if (x.isInstanceOf[ConstantSymbol]) {
        val replacement = createVariable(x)
        (createAtom(atom.pred.name, replacement), createAtom("{" + x + "}", replacement))
      } else (atom, null) // nothing has to be changed
      
    case x :: y :: Nil => if (x == y) (atom, null)
    else if (x.isInstanceOf[ConstantSymbol]) { // x is a constant=> simply append it
      val replacement = createVariable(x)
      (createAtom(atom.pred.name, replacement, y), createAtom("{" + x + "}", replacement))
    } else if (y.isInstanceOf[ConstantSymbol]) {
      val replacement = createVariable(y)
      (createAtom(atom.pred.name, x, replacement), createAtom("{" + y + "}", replacement))
    } else (atom, null)

  }

  def createVariable(constant: DatalogTerm): Variable = {
    val newVariable = Variable("x~" + constant + variablecounter)
    variablecounter += 1
    newVariable
  }

  def normalizePartially(rule: DatalogRule): DatalogRule = {
    val variables = for (term <- rule.givenResolution.terms if (term.isInstanceOf[Variable])) yield term.asInstanceOf[Variable]
    val occurringVariables = for (variable <- variables if (!occurrs(variable, rule.atomList))) yield variable
    val newAtoms = occurringVariables.map(createAtom("Top", _))

    new DatalogRule((rule.atomList) ::: newAtoms, rule.givenResolution)
  }

  def occurrs(v: Variable, atoms: List[DatalogAtom]): Boolean = atoms match {
    case Nil => false
    case x :: xs => if (x.terms.contains(v)) true else occurrs(v, xs)
  }

}